((LISP (NIL . (DECL (U V W) (OT& . GROUND) VARIABLE LIST) . NIL . ((W . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . W .)) (U . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . U .)) (LIST . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . LIST . PREFIX . 1000 .) . 1 . LIST .)) (V . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . V .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 1 .) (NIL . (DECL (X Y Z) (OT& . GROUND) VARIABLE SEXP) . NIL . ((Z . (VARIABLE . GROUND . SEXP . NIL . NIL . 2 . Z .)) (X . (VARIABLE . GROUND . SEXP . NIL . NIL . 2 . X .)) (SEXP . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . SEXP . PREFIX . 1000 .) . 2 . SEXP .)) (Y . (VARIABLE . GROUND . SEXP . NIL . NIL . 2 . Y .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 2 .) (NIL . (DECL (A B C) (OT& . GROUND) VARIABLE) . NIL . ((C . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 3 . C .)) (A . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 3 . A .)) (B . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 3 . B .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 3 .) (NIL . (DECL (PHI) (OT& (GROUND) . TRUTHVAL) VARIABLE) . NIL . ((PHI . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 4 . PHI .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 4 .) (NIL . (DECL (NNIL) (OT& . GROUND) CONSTANT LIST) . NIL . ((NNIL . (CONSTANT . GROUND . LIST . NIL . NIL . 5 . NNIL .)) (LIST . 1)) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 5 .) (NIL . (DECL (CONS) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((CONS . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 6 . CONS .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 6 .) (NIL . (DECL (CAR CDR) (OT& (GROUND) . GROUND) CONSTANT) . NIL . ((CDR . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 7 . CDR .)) (CAR . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 7 . CAR .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 7 .) (NIL . (DECL (NULL) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL . ((NULL . (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 8 . NULL .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 8 .) (NIL . (DECL (LIST) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL . ((LIST . (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 9 . LIST .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 9 .) (NIL . (DECL (SEXP) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL . ((SEXP . (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 10 . SEXP .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 10 .) ((((∀ U)) (LIST U)) . (AXIOM (TM& ((∀ U)) (LIST U))) . NIL . ((U . 1) (LIST . 9)) . NIL . NIL . NIL . (11) . NIL . LISP . NIL . NIL . 11 .) ((((∀ U)) (SEXP U)) . (AXIOM (TM& ((∀ U)) (SEXP U))) . NIL . ((U . 1) (SEXP . 10)) . NIL . NIL . NIL . (12) . NIL . LISP . NIL . NIL . 12 .) ((((∀ X)) (SEXP X)) . (AXIOM (TM& ((∀ X)) (SEXP X))) . NIL . ((X . 2) (SEXP . 10)) . NIL . NIL . NIL . (13) . NIL . LISP . NIL . NIL . 13 .) ((((∀ X U)) (LIST (CONS X U))) . (AXIOM (TM& ((∀ X U)) (LIST (CONS X U)))) . NIL . ((U . 1) (X . 2) (CONS . 6) (LIST . 9)) . NIL . NIL . NIL . (14) . NIL . LISP . NIL . NIL . 14 .) ((((∀ U)) (≡ (NULL U) (= U NNIL))) . (AXIOM (TM& ((∀ U)) (≡ (NULL U) (= U NNIL)))) . NIL . ((U . 1) (NNIL . 5) (NULL . 8)) . NIL . NIL . NIL . (15) . NIL . LISP . NIL . NIL . 15 .) ((((∀ X U)) (¬ (NULL (CONS X U)))) . (AXIOM (TM& ((∀ X U)) (¬ (NULL (CONS X U))))) . NIL . ((U . 1) (X . 2) (CONS . 6) (NULL . 8)) . NIL . NIL . NIL . (16) . NIL . LISP . NIL . NIL . 16 .) ((((∀ X U)) (= (CAR (CONS X U)) X)) . (AXIOM (TM& ((∀ X U)) (= (CAR (CONS X U)) X))) . NIL . ((U . 1) (X . 2) (CONS . 6) (CAR . 7)) . NIL . NIL . NIL . (17) . NIL . LISP . NIL . NIL . 17 .) ((((∀ X U)) (= (CDR (CONS X U)) U)) . (AXIOM (TM& ((∀ X U)) (= (CDR (CONS X U)) U))) . NIL . ((U . 1) (X . 2) (CONS . 6) (CDR . 7)) . NIL . NIL . NIL . (18) . NIL . LISP . NIL . NIL . 18 .) (NIL . (DECL (COPY) (OT& (GROUND) . GROUND) CONSTANT) . NIL . ((COPY . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 19 . COPY .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 19 .) ((((∀ U)) (= (COPY U) (CONDI (NULL U) NNIL (CONS (CAR U) (COPY (CDR U)))))) . (AXIOM (TM& ((∀ U)) (= (COPY U) (CONDI (NULL U) NNIL (CONS (CAR U) (COPY (CDR U))))))) . NIL . ((U . 1) (NNIL . 5) (CONS . 6) (CAR . 7) (CDR . 7) (NULL . 8) (COPY . 19)) . NIL . NIL . NIL . (20) . NIL . LISP . NIL . NIL . 20 .) ((((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (CONS X U))))) (((∀ U)) (PHI U)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (CONS X U))))) (((∀ U)) (PHI U))))) . NIL . ((U . 1) (X . 2) (PHI . 4) (NNIL . 5) (CONS . 6)) . NIL . NIL . NIL . (21) . NIL . LISP . NIL . NIL . 21 .) ((⊃ (∧ (= (COPY NNIL) NNIL) (((∀ X U)) (⊃ (= (COPY U) U) (= (COPY (CONS X U)) (CONS X U))))) (((∀ U)) (= (COPY U) U))) . (∀E PHI (TM& ((λ V)) (= (COPY V) V)) (LN& . 21) (LR& 14)) . NIL . ((U . 1) (X . 2) (NNIL . 5) (CONS . 6) (COPY . 19)) . NIL . NIL . NIL . (21 14) . NIL . LISP . NIL . NIL . 22 .) ((= (COPY (CONS X U)) (CONS X (COPY U))) . (TRMREWRITE (TM& COPY (CONS X U)) SRIGHT (LR& 20 16 17 18) (LR& 14)) . NIL . ((U . 1) (CONS . 6) (COPY . 19) (X . 2)) . NIL . NIL . NIL . (20 16 17 18 14) . NIL . LISP . NIL . NIL . 23 .) ((((∀ X U)) (= (COPY (CONS X U)) (CONS X (COPY U)))) . (∀I (X U) (LN& . 23)) . NIL . ((U . 1) (CONS . 6) (COPY . 19) (X . 2)) . NIL . NIL . NIL . (20 16 17 18 14) . NIL . LISP . NIL . NIL . 24 .) ((((∀ U)) (= (COPY U) U)) . (DECSIMP (TM& ((∀ U)) (= (COPY U) U)) SRIGHT (LR& 22) (LR&) (LR& 14) (LR& 20 15 24)) . NIL . ((COPY . 19) (U . 1)) . NIL . NIL . NIL . (14 18 17 16 20 15 21) . NIL . LISP . NIL . NIL . 25 .)))